es:ES, ds:x:Id fp Type, R:(State(ds)State(ds)).
(s, s':State(ds). Dec(R(s,s')))
 (e:{e:E| @loc(e) discrete ds} .
 e'e.R((state when e),state after e')
  e'e.R((state when e),state after e')
  e'e.& e''[e,e').(R((state when e),state after e''))) 

latex

Definitions	e[e1,e2).P(e), e'e.P(e'), x:A. B(x), {T}, A, Dec(P), P  Q, A c B, e loc e' , P & Q, x. t(x), t  T, P  Q, , a:A fp B(a), x:A. B(x), (e <loc e'), False, SQType(T), x(s)
Lemmas	es-le wf, alle-between1 wf, not wf, decidable and, decidable es-le, es-le-loc, es-locl wf, es-minimal-event, event system wf, l member wf, Id wf, decidable wf, decl-state wf, es-dds wf, es-E wf, Id sq, es-state-after wf, es-state-subtype2, es-state-when wf, es-loc wf, existse-ge wf